\functions {
int i844;
int i949;
int i1041;
int i1140;
int i1254;
int i1394;
}
\predicates {
}
\problem {
(true)
 &
(((((((((((((((((((((((((((((((((((((((((((((((((((
\part[left](((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((v_princess_137() & (((!((((v_princess_136) = ((0+(400)))) & (true)))) -> (!(v_princess_137()))) & (((((v_princess_136) = ((0+(400)))) & (true))) -> (v_princess_137())))))) & (((v_princess_136) = (v_princess_139) & (((!(((v_princess_117) = ((0+(229)))))) -> ((v_princess_139) = (v_princess_135))) & ((((v_princess_117) = ((0+(229))))) -> ((v_princess_139) = ((242)))))))))) & (((v_princess_135) = (v_princess_141) & (((!(((v_princess_117) = ((0+(243)))))) -> ((v_princess_141) = (v_princess_134))) & ((((v_princess_117) = ((0+(243))))) -> ((v_princess_141) = ((397)))))))))) & (((v_princess_134) = (v_princess_143) & (((!(((v_princess_117) = ((0+(40)))))) -> ((v_princess_143) = (v_princess_133))) & ((((v_princess_117) = ((0+(40))))) -> ((v_princess_143) = ((401)))))))))) & (((v_princess_133) = (v_princess_145) & (((!(((v_princess_117) = ((0+(43)))))) -> ((v_princess_145) = (v_princess_132))) & ((((v_princess_117) = ((0+(43))))) -> ((v_princess_145) = ((48)))))))))) & (((v_princess_132) = (v_princess_147) & (((!(((v_princess_117) = ((0+(398)))))) -> ((v_princess_147) = (v_princess_131))) & ((((v_princess_117) = ((0+(398))))) -> ((v_princess_147) = ((395)))))))))) & (((v_princess_131) = (v_princess_149) & (((!(((v_princess_117) = ((0+(395)))))) -> ((v_princess_149) = (v_princess_130))) & ((((v_princess_117) = ((0+(395))))) -> ((v_princess_149) = (v_princess_124))))))))) & (((v_princess_130) = (v_princess_151) & (((!(((v_princess_117) = ((0+(396)))))) -> ((v_princess_151) = (v_princess_129))) & ((((v_princess_117) = ((0+(396))))) -> ((v_princess_151) = ((250)))))))))) & (((v_princess_129) = (v_princess_153) & (((!(((v_princess_117) = ((0+(250)))))) -> ((v_princess_153) = (v_princess_128))) & ((((v_princess_117) = ((0+(250))))) -> ((v_princess_153) = ((251)))))))))) & (((v_princess_128) = (v_princess_155) & (((!(((v_princess_117) = ((0+(402)))))) -> ((v_princess_155) = (v_princess_127))) & ((((v_princess_117) = ((0+(402))))) -> ((v_princess_155) = ((399)))))))))) & (((v_princess_127) = (v_princess_157) & (((!(((v_princess_117) = ((0+(399)))))) -> ((v_princess_157) = (v_princess_126))) & ((((v_princess_117) = ((0+(399))))) -> ((v_princess_157) = (v_princess_121))))))))) & (((v_princess_126) = (v_princess_159) & (((!(((v_princess_117) = ((0+(50)))))) -> ((v_princess_159) = (v_princess_125))) & ((((v_princess_117) = ((0+(50))))) -> ((v_princess_159) = (v_princess_122))))))))) & (((v_princess_125) = (v_princess_161) & (((!(((v_princess_117) = ((0+(251)))))) -> ((v_princess_161) = (v_princess_123))) & ((((v_princess_117) = ((0+(251))))) -> ((v_princess_161) = ((254)))))))))) & (((v_princess_124) = (v_princess_163) & (((!(!((((v_princess_85) <= ((0+v_princess_83))))))) -> ((v_princess_163) = (v_princess_120))) & ((!((((v_princess_85) <= ((0+v_princess_83)))))) -> ((v_princess_163) = ((396)))))))))) & (((v_princess_123) = (v_princess_165) & (((!(((v_princess_117) = ((0+(252)))))) -> ((v_princess_165) = (v_princess_117))) & ((((v_princess_117) = ((0+(252))))) -> ((v_princess_165) = ((254)))))))))) & (((v_princess_122) = (v_princess_167) & (((!(((v_princess_103) = ((0+(13)))))) -> ((v_princess_167) = (v_princess_119))) & ((((v_princess_103) = ((0+(13))))) -> ((v_princess_167) = ((373)))))))))) & (((v_princess_121) = (v_princess_169) & (((!(!((((v_princess_88) <= ((0+v_princess_86))))))) -> ((v_princess_169) = (v_princess_118))) & ((!((((v_princess_88) <= ((0+v_princess_86)))))) -> ((v_princess_169) = ((400)))))))))) & (((v_princess_120) = (v_princess_171) & (((!((((v_princess_85) <= ((0+v_princess_83)))))) -> ((v_princess_171) = (v_princess_117))) & (((((v_princess_85) <= ((0+v_princess_83))))) -> ((v_princess_171) = ((250))))))))))))))))))))))) & (((v_princess_119) = (v_princess_173) & (((!(!(((v_princess_103) = ((0+(13))))))) -> ((v_princess_173) = (v_princess_117))) & ((!(((v_princess_103) = ((0+(13)))))) -> ((v_princess_173) = ((54)))))))))) & (((v_princess_118) = (v_princess_175) & (((!((((v_princess_88) <= ((0+v_princess_86)))))) -> ((v_princess_175) = (v_princess_117))) & (((((v_princess_88) <= ((0+v_princess_86))))) -> ((v_princess_175) = ((222)))))))))) & (((v_princess_117) = (v_princess_177) & (((!(((v_princess_100) = ((0+(227)))))) -> ((v_princess_177) = (v_princess_116))) & ((((v_princess_100) = ((0+(227))))) -> ((v_princess_177) = ((229)))))))))) & (((v_princess_116) = (v_princess_179) & (((!(((v_princess_100) = ((0+(242)))))) -> ((v_princess_179) = (v_princess_115))) & ((((v_princess_100) = ((0+(242))))) -> ((v_princess_179) = ((243)))))))))) & (((v_princess_115) = (v_princess_181) & (((!(((v_princess_100) = ((0+(39)))))) -> ((v_princess_181) = (v_princess_114))) & ((((v_princess_100) = ((0+(39))))) -> ((v_princess_181) = ((40)))))))))) & (((v_princess_114) = (v_princess_183) & (((!(((v_princess_100) = ((0+(42)))))) -> ((v_princess_183) = (v_princess_113))) & ((((v_princess_100) = ((0+(42))))) -> ((v_princess_183) = ((43)))))))))) & (((v_princess_113) = (v_princess_185) & (((!(((v_princess_100) = ((0+(397)))))) -> ((v_princess_185) = (v_princess_112))) & ((((v_princess_100) = ((0+(397))))) -> ((v_princess_185) = (v_princess_108))))))))) & (((v_princess_112) = (v_princess_187) & (((!(((v_princess_100) = ((0+(395)))))) -> ((v_princess_187) = (v_princess_111))) & ((((v_princess_100) = ((0+(395))))) -> ((v_princess_187) = (v_princess_105))))))))) & (((v_princess_111) = (v_princess_189) & (((!(((v_princess_100) = ((0+(401)))))) -> ((v_princess_189) = (v_princess_110))) & ((((v_princess_100) = ((0+(401))))) -> ((v_princess_189) = (v_princess_106))))))))) & (((v_princess_110) = (v_princess_191) & (((!(((v_princess_100) = ((0+(48)))))) -> ((v_princess_191) = (v_princess_109))) & ((((v_princess_100) = ((0+(48))))) -> ((v_princess_191) = ((50)))))))))) & (((v_princess_109) = (v_princess_193) & (((!(((v_princess_100) = ((0+(396)))))) -> ((v_princess_193) = (v_princess_107))) & ((((v_princess_100) = ((0+(396))))) -> ((v_princess_193) = ((250)))))))))) & (((v_princess_108) = (v_princess_195) & (((!(!((((v_princess_83) <= ((0+v_princess_84))))))) -> ((v_princess_195) = (v_princess_104))) & ((!((((v_princess_83) <= ((0+v_princess_84)))))) -> ((v_princess_195) = ((398))))))))))) & (((v_princess_107) = (v_princess_197) & (((!(((v_princess_100) = ((0+(250)))))) -> ((v_princess_197) = (v_princess_100))) & ((((v_princess_100) = ((0+(250))))) -> ((v_princess_197) = ((251)))))))))) & (((v_princess_106) = (v_princess_199) & (((!(!((((v_princess_86) <= ((0+v_princess_87))))))) -> ((v_princess_199) = (v_princess_102))) & ((!((((v_princess_86) <= ((0+v_princess_87)))))) -> ((v_princess_199) = ((402)))))))))) & (((v_princess_105) = (v_princess_201) & (((!(!((((v_princess_85) <= ((0+v_princess_83))))))) -> ((v_princess_201) = (v_princess_101))) & ((!((((v_princess_85) <= ((0+v_princess_83)))))) -> ((v_princess_201) = ((396)))))))))) & (((v_princess_104) = (v_princess_203) & (((!((((v_princess_83) <= ((0+v_princess_84)))))) -> ((v_princess_203) = (v_princess_100))) & (((((v_princess_83) <= ((0+v_princess_84))))) -> ((v_princess_203) = ((395)))))))))) & (((v_princess_103) = (v_princess_205) & (((!(!(((v_princess_100) = ((0+(48))))))) -> ((v_princess_205) = (i1394))) & ((!(((v_princess_100) = ((0+(48)))))) -> ((v_princess_205) = ((0)))))))))))))))))))) & (((v_princess_102) = (v_princess_207) & (((!((((v_princess_86) <= ((0+v_princess_87)))))) -> ((v_princess_207) = (v_princess_100))) & (((((v_princess_86) <= ((0+v_princess_87))))) -> ((v_princess_207) = ((399)))))))))) & (((v_princess_101) = (v_princess_209) & (((!((((v_princess_85) <= ((0+v_princess_83)))))) -> ((v_princess_209) = (v_princess_100))) & (((((v_princess_85) <= ((0+v_princess_83))))) -> ((v_princess_209) = ((250)))))))))) & (((v_princess_100) = (v_princess_211) & (((!(((v_princess_80) = ((0+(224)))))) -> ((v_princess_211) = (v_princess_99))) & ((((v_princess_80) = ((0+(224))))) -> ((v_princess_211) = (v_princess_92))))))))) & (((v_princess_99) = (v_princess_213) & (((!(((v_princess_80) = ((0+(38)))))) -> ((v_princess_213) = (v_princess_98))) & ((((v_princess_80) = ((0+(38))))) -> ((v_princess_213) = (v_princess_90))))))))) & (((v_princess_98) = (v_princess_215) & (((!(((v_princess_80) = ((0+(229)))))) -> ((v_princess_215) = (v_princess_97))) & ((((v_princess_80) = ((0+(229))))) -> ((v_princess_215) = ((242)))))))))) & (((v_princess_97) = (v_princess_217) & (((!(((v_princess_80) = ((0+(243)))))) -> ((v_princess_217) = (v_princess_96))) & ((((v_princess_80) = ((0+(243))))) -> ((v_princess_217) = ((397)))))))))) & (((v_princess_96) = (v_princess_219) & (((!(((v_princess_80) = ((0+(40)))))) -> ((v_princess_219) = (v_princess_95))) & ((((v_princess_80) = ((0+(40))))) -> ((v_princess_219) = ((401)))))))))) & (((v_princess_95) = (v_princess_221) & (((!(((v_princess_80) = ((0+(43)))))) -> ((v_princess_221) = (v_princess_94))) & ((((v_princess_80) = ((0+(43))))) -> ((v_princess_221) = ((48)))))))))) & (((v_princess_94) = (v_princess_223) & (((!(((v_princess_80) = ((0+(398)))))) -> ((v_princess_223) = (v_princess_93))) & ((((v_princess_80) = ((0+(398))))) -> ((v_princess_223) = ((395)))))))))) & (((v_princess_93) = (v_princess_225) & (((!(!(((v_princess_80) = ((0+(395))))))) -> ((v_princess_225) = (v_princess_91))) & ((!(((v_princess_80) = ((0+(395)))))) -> ((v_princess_225) = (v_princess_80))))))))) & (((v_princess_92) = (v_princess_227) & (((!(!(((v_princess_66) = ((0+(0))))))) -> ((v_princess_227) = (v_princess_89))) & ((!(((v_princess_66) = ((0+(0)))))) -> ((v_princess_227) = ((227)))))))))))))) & (((v_princess_91) = (v_princess_229) & (((!(!((((v_princess_55) <= ((0+v_princess_53))))))) -> ((v_princess_229) = (v_princess_82))) & ((!((((v_princess_55) <= ((0+v_princess_53)))))) -> ((v_princess_229) = ((396)))))))))) & (((v_princess_90) = (v_princess_231) & (((!(((v_princess_67) = ((0+((0) - ((1)))))))) -> ((v_princess_231) = (v_princess_81))) & ((((v_princess_67) = ((0+((0) - ((1))))))) -> ((v_princess_231) = ((39)))))))))) & (((v_princess_89) = (v_princess_233) & (((!(((v_princess_66) = ((0+(0)))))) -> ((v_princess_233) = (v_princess_80))) & ((((v_princess_66) = ((0+(0))))) -> ((v_princess_233) = ((242)))))))))) & (((v_princess_88) = (v_princess_235) & (((!(!(((v_princess_80) = ((0+(40))))))) -> ((v_princess_235) = (v_princess_71))) & ((!(((v_princess_80) = ((0+(40)))))) -> ((v_princess_235) = ((0)))))))))) & (((v_princess_87) = (v_princess_237) & (((!(!(((v_princess_80) = ((0+(40))))))) -> ((v_princess_237) = (v_princess_70))) & ((!(((v_princess_80) = ((0+(40)))))) -> ((v_princess_237) = ((0)))))))))) & (((v_princess_86) = (v_princess_239) & (((!(!(((v_princess_80) = ((0+(40))))))) -> ((v_princess_239) = (v_princess_69))) & ((!(((v_princess_80) = ((0+(40)))))) -> ((v_princess_239) = ((0)))))))))) & (((v_princess_85) = (v_princess_241) & (((!(((v_princess_80) = ((0+(243)))))) -> ((v_princess_241) = (v_princess_55))) & ((((v_princess_80) = ((0+(243))))) -> ((v_princess_241) = (v_princess_18))))))))) & (((v_princess_84) = (v_princess_243) & (((!(((v_princess_80) = ((0+(243)))))) -> ((v_princess_243) = (v_princess_54))) & ((((v_princess_80) = ((0+(243))))) -> ((v_princess_243) = (v_princess_17))))))))) & (((v_princess_83) = (v_princess_245) & (((!(!(((v_princess_80) = ((0+(243))))))) -> ((v_princess_245) = (v_princess_73))) & ((!(((v_princess_80) = ((0+(243)))))) -> ((v_princess_245) = (v_princess_53))))))))))))))))) & (((v_princess_82) = (v_princess_247) & (((!((((v_princess_55) <= ((0+v_princess_53)))))) -> ((v_princess_247) = (v_princess_80))) & (((((v_princess_55) <= ((0+v_princess_53))))) -> ((v_princess_247) = ((250)))))))))) & (((v_princess_81) = (v_princess_249) & (((!(!(((v_princess_67) = ((0+((0) - ((1))))))))) -> ((v_princess_249) = (v_princess_80))) & ((!(((v_princess_67) = ((0+((0) - ((1)))))))) -> ((v_princess_249) = ((42)))))))))) & (((v_princess_80) = (v_princess_251) & (((!(((v_princess_64) = ((0+(222)))))) -> ((v_princess_251) = (v_princess_79))) & ((((v_princess_64) = ((0+(222))))) -> ((v_princess_251) = ((224)))))))))) & (((v_princess_79) = (v_princess_253) & (((!(((v_princess_64) = ((0+(36)))))) -> ((v_princess_253) = (v_princess_78))) & ((((v_princess_64) = ((0+(36))))) -> ((v_princess_253) = ((38)))))))))) & (((v_princess_78) = (v_princess_255) & (((!(((v_princess_64) = ((0+(227)))))) -> ((v_princess_255) = (v_princess_77))) & ((((v_princess_64) = ((0+(227))))) -> ((v_princess_255) = ((229)))))))))) & (((v_princess_77) = (v_princess_257) & (((!(((v_princess_64) = ((0+(242)))))) -> ((v_princess_257) = (v_princess_76))) & ((((v_princess_64) = ((0+(242))))) -> ((v_princess_257) = ((243)))))))))) & (((v_princess_76) = (v_princess_259) & (((!(((v_princess_64) = ((0+(39)))))) -> ((v_princess_259) = (v_princess_75))) & ((((v_princess_64) = ((0+(39))))) -> ((v_princess_259) = ((40)))))))))) & (((v_princess_75) = (v_princess_261) & (((!(((v_princess_64) = ((0+(42)))))) -> ((v_princess_261) = (v_princess_74))) & ((((v_princess_64) = ((0+(42))))) -> ((v_princess_261) = ((43)))))))))) & (((v_princess_74) = (v_princess_263) & (((!(!(((v_princess_64) = ((0+(397))))))) -> ((v_princess_263) = (v_princess_72))) & ((!(((v_princess_64) = ((0+(397)))))) -> ((v_princess_263) = (v_princess_64))))))))) & (v_princess_73) = (((v_princess_15*1)+(v_princess_68*1)+0))))))) & (((v_princess_72) = (v_princess_265) & (((!(!((((v_princess_53) <= ((0+v_princess_54))))))) -> ((v_princess_265) = (v_princess_65))) & ((!((((v_princess_53) <= ((0+v_princess_54)))))) -> ((v_princess_265) = ((398)))))))))) & (((v_princess_71) = (v_princess_267) & (((!(!(((v_princess_64) = ((0+(39))))))) -> ((v_princess_267) = (v_princess_18))) & ((!(((v_princess_64) = ((0+(39)))))) -> ((v_princess_267) = ((0)))))))))) & (((v_princess_70) = (v_princess_269) & (((!(!(((v_princess_64) = ((0+(39))))))) -> ((v_princess_269) = (v_princess_17))) & ((!(((v_princess_64) = ((0+(39)))))) -> ((v_princess_269) = ((0)))))))))) & (((v_princess_69) = (v_princess_271) & (((!(!(((v_princess_64) = ((0+(39))))))) -> ((v_princess_271) = (v_princess_15))) & ((!(((v_princess_64) = ((0+(39)))))) -> ((v_princess_271) = ((0)))))))))) & (((v_princess_68) = (v_princess_273) & (((!(!(((v_princess_64) = ((0+(242))))))) -> ((v_princess_273) = (i1254))) & ((!(((v_princess_64) = ((0+(242)))))) -> ((v_princess_273) = (v_princess_44))))))))) & (((v_princess_67) = (v_princess_275) & (((!(!(((v_princess_64) = ((0+(36))))))) -> ((v_princess_275) = (i1254))) & ((!(((v_princess_64) = ((0+(36)))))) -> ((v_princess_275) = (v_princess_43))))))))) & (((v_princess_66) = (v_princess_277) & (((!(!(((v_princess_64) = ((0+(222))))))) -> ((v_princess_277) = (i1254))) & ((!(((v_princess_64) = ((0+(222)))))) -> ((v_princess_277) = (v_princess_42)))))))))))))))) & (((v_princess_65) = (v_princess_279) & (((!((((v_princess_53) <= ((0+v_princess_54)))))) -> ((v_princess_279) = (v_princess_64))) & (((((v_princess_53) <= ((0+v_princess_54))))) -> ((v_princess_279) = ((395)))))))))) & (((v_princess_64) = (v_princess_281) & (((!(((v_princess_50) = ((0+(35)))))) -> ((v_princess_281) = (v_princess_63))) & ((((v_princess_50) = ((0+(35))))) -> ((v_princess_281) = (v_princess_60))))))))) & (((v_princess_63) = (v_princess_283) & (((!(((v_princess_50) = ((0+(224)))))) -> ((v_princess_283) = (v_princess_62))) & ((((v_princess_50) = ((0+(224))))) -> ((v_princess_283) = (v_princess_57))))))))) & (((v_princess_62) = (v_princess_285) & (((!(((v_princess_50) = ((0+(38)))))) -> ((v_princess_285) = (v_princess_61))) & ((((v_princess_50) = ((0+(38))))) -> ((v_princess_285) = (v_princess_58))))))))) & (((v_princess_61) = (v_princess_287) & (((!(((v_princess_50) = ((0+(229)))))) -> ((v_princess_287) = (v_princess_59))) & ((((v_princess_50) = ((0+(229))))) -> ((v_princess_287) = ((242)))))))))) & (((v_princess_60) = (v_princess_289) & (((!((((v_princess_41) <= ((0+(14))))))) -> ((v_princess_289) = (v_princess_56))) & (((((v_princess_41) <= ((0+(14)))))) -> ((v_princess_289) = ((36)))))))))))) & (((v_princess_59) = (v_princess_291) & (((!(((v_princess_50) = ((0+(243)))))) -> ((v_princess_291) = (v_princess_50))) & ((((v_princess_50) = ((0+(243))))) -> ((v_princess_291) = ((397)))))))))) & (((v_princess_58) = (v_princess_293) & (((!(((v_princess_43) = ((0+((0) - ((1)))))))) -> ((v_princess_293) = (v_princess_52))) & ((((v_princess_43) = ((0+((0) - ((1))))))) -> ((v_princess_293) = ((39)))))))))) & (((v_princess_57) = (v_princess_295) & (((!(!(((v_princess_42) = ((0+(0))))))) -> ((v_princess_295) = (v_princess_51))) & ((!(((v_princess_42) = ((0+(0)))))) -> ((v_princess_295) = ((227)))))))))) & (((v_princess_56) = (v_princess_297) & (((!(!((((v_princess_41) <= ((0+(14)))))))) -> ((v_princess_297) = (v_princess_50))) & ((!((((v_princess_41) <= ((0+(14))))))) -> ((v_princess_297) = ((222)))))))))) & (((v_princess_55) = (v_princess_299) & (((!(!(((v_princess_50) = ((0+(243))))))) -> ((v_princess_299) = (v_princess_18))) & ((!(((v_princess_50) = ((0+(243)))))) -> ((v_princess_299) = ((0)))))))))) & (((v_princess_54) = (v_princess_301) & (((!(!(((v_princess_50) = ((0+(243))))))) -> ((v_princess_301) = (v_princess_17))) & ((!(((v_princess_50) = ((0+(243)))))) -> ((v_princess_301) = ((0)))))))))) & (((v_princess_53) = (v_princess_303) & (((!(!(((v_princess_50) = ((0+(243))))))) -> ((v_princess_303) = (v_princess_46))) & ((!(((v_princess_50) = ((0+(243)))))) -> ((v_princess_303) = ((0))))))))))))))) & (((v_princess_52) = (v_princess_305) & (((!(!(((v_princess_43) = ((0+((0) - ((1))))))))) -> ((v_princess_305) = (v_princess_50))) & ((!(((v_princess_43) = ((0+((0) - ((1)))))))) -> ((v_princess_305) = ((42)))))))))) & (((v_princess_51) = (v_princess_307) & (((!(((v_princess_42) = ((0+(0)))))) -> ((v_princess_307) = (v_princess_50))) & ((((v_princess_42) = ((0+(0))))) -> ((v_princess_307) = ((242)))))))))) & (((v_princess_50) = (v_princess_309) & (((!(((v_princess_40) = ((0+(33)))))) -> ((v_princess_309) = (v_princess_49))) & ((((v_princess_40) = ((0+(33))))) -> ((v_princess_309) = ((35)))))))))) & (((v_princess_49) = (v_princess_311) & (((!(((v_princess_40) = ((0+(222)))))) -> ((v_princess_311) = (v_princess_48))) & ((((v_princess_40) = ((0+(222))))) -> ((v_princess_311) = ((224)))))))))) & (((v_princess_48) = (v_princess_313) & (((!(((v_princess_40) = ((0+(36)))))) -> ((v_princess_313) = (v_princess_47))) & ((((v_princess_40) = ((0+(36))))) -> ((v_princess_313) = ((38)))))))))) & (((v_princess_47) = (v_princess_315) & (((!(((v_princess_40) = ((0+(227)))))) -> ((v_princess_315) = (v_princess_45))) & ((((v_princess_40) = ((0+(227))))) -> ((v_princess_315) = ((229)))))))))) & (v_princess_46) = (((v_princess_15*1)+(v_princess_44*1)+0)))))))) & (((v_princess_45) = (v_princess_317) & (((!(((v_princess_40) = ((0+(242)))))) -> ((v_princess_317) = (v_princess_40))) & ((((v_princess_40) = ((0+(242))))) -> ((v_princess_317) = ((243)))))))))) & (((v_princess_44) = (v_princess_319) & (((!(!(((v_princess_40) = ((0+(242))))))) -> ((v_princess_319) = (i1140))) & ((!(((v_princess_40) = ((0+(242)))))) -> ((v_princess_319) = ((0)))))))))) & (((v_princess_43) = (v_princess_321) & (((!(!(((v_princess_40) = ((0+(36))))))) -> ((v_princess_321) = (i1140))) & ((!(((v_princess_40) = ((0+(36)))))) -> ((v_princess_321) = ((0)))))))))) & (((v_princess_42) = (v_princess_323) & (((!(!(((v_princess_40) = ((0+(222))))))) -> ((v_princess_323) = (i1140))) & ((!(((v_princess_40) = ((0+(222)))))) -> ((v_princess_323) = (v_princess_28))))))))) & (((v_princess_41) = (v_princess_325) & (((!(!(((v_princess_40) = ((0+(33))))))) -> ((v_princess_325) = (i1140))) & ((!(((v_princess_40) = ((0+(33)))))) -> ((v_princess_325) = (v_princess_27)))))))))))))) & (((v_princess_40) = (v_princess_327) & (((!(((v_princess_31) = ((0+(32)))))) -> ((v_princess_327) = (v_princess_39))) & ((((v_princess_31) = ((0+(32))))) -> ((v_princess_327) = (v_princess_37))))))))) & (((v_princess_39) = (v_princess_329) & (((!(((v_princess_31) = ((0+(35)))))) -> ((v_princess_329) = (v_princess_38))) & ((((v_princess_31) = ((0+(35))))) -> ((v_princess_329) = (v_princess_35))))))))) & (((v_princess_38) = (v_princess_331) & (((!(!(((v_princess_31) = ((0+(224))))))) -> ((v_princess_331) = (v_princess_36))) & ((!(((v_princess_31) = ((0+(224)))))) -> ((v_princess_331) = (v_princess_31))))))))) & (((v_princess_37) = (v_princess_333) & (((!(!(((v_princess_26) = ((0+(0))))))) -> ((v_princess_333) = (v_princess_34))) & ((!(((v_princess_26) = ((0+(0)))))) -> ((v_princess_333) = ((33)))))))))) & (((v_princess_36) = (v_princess_335) & (((!(!(((v_princess_28) = ((0+(0))))))) -> ((v_princess_335) = (v_princess_33))) & ((!(((v_princess_28) = ((0+(0)))))) -> ((v_princess_335) = ((227)))))))))) & (((v_princess_35) = (v_princess_337) & (((!((((v_princess_27) <= ((0+(14))))))) -> ((v_princess_337) = (v_princess_32))) & (((((v_princess_27) <= ((0+(14)))))) -> ((v_princess_337) = ((36)))))))))) & (((v_princess_34) = (v_princess_339) & (((!(((v_princess_26) = ((0+(0)))))) -> ((v_princess_339) = (v_princess_31))) & ((((v_princess_26) = ((0+(0))))) -> ((v_princess_339) = ((222))))))))))))) & (((v_princess_33) = (v_princess_341) & (((!(((v_princess_28) = ((0+(0)))))) -> ((v_princess_341) = (v_princess_31))) & ((((v_princess_28) = ((0+(0))))) -> ((v_princess_341) = ((242)))))))))) & (((v_princess_32) = (v_princess_343) & (((!(!((((v_princess_27) <= ((0+(14)))))))) -> ((v_princess_343) = (v_princess_31))) & ((!((((v_princess_27) <= ((0+(14))))))) -> ((v_princess_343) = ((222)))))))))) & (((v_princess_31) = (v_princess_345) & (((!(((v_princess_25) = ((0+(30)))))) -> ((v_princess_345) = (v_princess_30))) & ((((v_princess_25) = ((0+(30))))) -> ((v_princess_345) = ((32)))))))))) & (((v_princess_30) = (v_princess_347) & (((!(((v_princess_25) = ((0+(33)))))) -> ((v_princess_347) = (v_princess_29))) & ((((v_princess_25) = ((0+(33))))) -> ((v_princess_347) = ((35))))))))))))) & (((v_princess_29) = (v_princess_349) & (((!(((v_princess_25) = ((0+(222)))))) -> ((v_princess_349) = (v_princess_25))) & ((((v_princess_25) = ((0+(222))))) -> ((v_princess_349) = ((224)))))))))) & (((v_princess_28) = (v_princess_351) & (((!(!(((v_princess_25) = ((0+(222))))))) -> ((v_princess_351) = (i1041))) & ((!(((v_princess_25) = ((0+(222)))))) -> ((v_princess_351) = ((0)))))))))) & (((v_princess_27) = (v_princess_353) & (((!(!(((v_princess_25) = ((0+(33))))))) -> ((v_princess_353) = (i1041))) & ((!(((v_princess_25) = ((0+(33)))))) -> ((v_princess_353) = ((0)))))))))) & (((v_princess_26) = (v_princess_355) & (((!(!(((v_princess_25) = ((0+(30))))))) -> ((v_princess_355) = (i1041))) & ((!(((v_princess_25) = ((0+(30)))))) -> ((v_princess_355) = (v_princess_16)))))))))))) & (((v_princess_25) = (v_princess_357) & (((!(((v_princess_20) = ((0+(25)))))) -> ((v_princess_357) = (v_princess_24))) & ((((v_princess_20) = ((0+(25))))) -> ((v_princess_357) = (v_princess_22))))))))) & (((v_princess_24) = (v_princess_359) & (((!(!(((v_princess_20) = ((0+(32))))))) -> ((v_princess_359) = (v_princess_23))) & ((!(((v_princess_20) = ((0+(32)))))) -> ((v_princess_359) = (v_princess_20))))))))) & (((v_princess_23) = (v_princess_361) & (((!(!(((v_princess_16) = ((0+(0))))))) -> ((v_princess_361) = (v_princess_21))) & ((!(((v_princess_16) = ((0+(0)))))) -> ((v_princess_361) = ((33)))))))))) & (((v_princess_22) = (v_princess_363) & (((!(!((((v_princess_15) <= ((0+(0)))))))) -> ((v_princess_363) = (v_princess_20))) & ((!((((v_princess_15) <= ((0+(0))))))) -> ((v_princess_363) = ((30)))))))))))) & (((v_princess_21) = (v_princess_365) & (((!(((v_princess_16) = ((0+(0)))))) -> ((v_princess_365) = (v_princess_20))) & ((((v_princess_16) = ((0+(0))))) -> ((v_princess_365) = ((222)))))))))) & (((v_princess_20) = (v_princess_367) & (((!(((v_princess_14) = ((0+(23)))))) -> ((v_princess_367) = (v_princess_19))) & ((((v_princess_14) = ((0+(23))))) -> ((v_princess_367) = ((25)))))))))))) & (((v_princess_19) = (v_princess_369) & (((!(((v_princess_14) = ((0+(30)))))) -> ((v_princess_369) = (v_princess_14))) & ((((v_princess_14) = ((0+(30))))) -> ((v_princess_369) = ((32)))))))))) & (((v_princess_18) = (v_princess_371) & (((!(!(((v_princess_14) = ((0+(23))))))) -> ((v_princess_371) = (v_princess_8))) & ((!(((v_princess_14) = ((0+(23)))))) -> ((v_princess_371) = ((0)))))))))) & (((v_princess_17) = (v_princess_373) & (((!(!(((v_princess_14) = ((0+(23))))))) -> ((v_princess_373) = (v_princess_11))) & ((!(((v_princess_14) = ((0+(23)))))) -> ((v_princess_373) = (v_princess_7))))))))) & (((v_princess_16) = (v_princess_375) & (((!(!(((v_princess_14) = ((0+(30))))))) -> ((v_princess_375) = (i949))) & ((!(((v_princess_14) = ((0+(30)))))) -> ((v_princess_375) = ((0)))))))))) & (((v_princess_15) = (v_princess_377) & (((!(((v_princess_14) = ((0+(23)))))) -> ((v_princess_377) = (v_princess_6))) & ((((v_princess_14) = ((0+(23))))) -> ((v_princess_377) = (v_princess_2))))))))))) & (((v_princess_14) = (v_princess_379) & (((!(((v_princess_10) = ((0+(25)))))) -> ((v_princess_379) = (v_princess_13))) & ((((v_princess_10) = ((0+(25))))) -> ((v_princess_379) = (v_princess_12))))))))) & (((v_princess_13) = (v_princess_381) & (((!(((v_princess_10) = ((0+(21)))))) -> ((v_princess_381) = (v_princess_10))) & ((((v_princess_10) = ((0+(21))))) -> ((v_princess_381) = ((23)))))))))) & (((v_princess_12) = (v_princess_383) & (((!(!((((v_princess_6) <= ((0+(0)))))))) -> ((v_princess_383) = (v_princess_10))) & ((!((((v_princess_6) <= ((0+(0))))))) -> ((v_princess_383) = ((30)))))))))) & (((v_princess_11) = (v_princess_385) & (((!(((v_princess_10) = ((0+(21)))))) -> ((v_princess_385) = (v_princess_3))) & ((((v_princess_10) = ((0+(21))))) -> ((v_princess_385) = ((145)))))))))))) & (((v_princess_10) = (v_princess_387) & (((!(((v_princess_5) = ((0+(19)))))) -> ((v_princess_387) = (v_princess_9))) & ((((v_princess_5) = ((0+(19))))) -> ((v_princess_387) = ((21))))))))))) & (((v_princess_9) = (v_princess_389) & (((!(((v_princess_5) = ((0+(23)))))) -> ((v_princess_389) = (v_princess_5))) & ((((v_princess_5) = ((0+(23))))) -> ((v_princess_389) = ((25)))))))))) & (((v_princess_8) = (v_princess_391) & (((!(!(((v_princess_5) = ((0+(19))))))) -> ((v_princess_391) = ((143)))) & ((!(((v_princess_5) = ((0+(19)))))) -> ((v_princess_391) = ((0)))))))))) & (((v_princess_7) = (v_princess_393) & (((!(!(((v_princess_5) = ((0+(23))))))) -> ((v_princess_393) = (v_princess_3))) & ((!(((v_princess_5) = ((0+(23)))))) -> ((v_princess_393) = ((0)))))))))) & (((v_princess_6) = (v_princess_395) & (((!(!(((v_princess_5) = ((0+(23))))))) -> ((v_princess_395) = (v_princess_2))) & ((!(((v_princess_5) = ((0+(23)))))) -> ((v_princess_395) = ((0)))))))))))) & (((v_princess_5) = (v_princess_397) & (((!(((v_princess_1) = ((0+(18)))))) -> ((v_princess_397) = (v_princess_4))) & ((((v_princess_1) = ((0+(18))))) -> ((v_princess_397) = ((19)))))))))) & (((v_princess_4) = (v_princess_399) & (((!(((v_princess_1) = ((0+(22)))))) -> ((v_princess_399) = (v_princess_1))) & ((((v_princess_1) = ((0+(22))))) -> ((v_princess_399) = ((23)))))))))) & (((v_princess_3) = (v_princess_401) & (((!(!(((v_princess_1) = ((0+(22))))))) -> ((v_princess_401) = (((0) - ((1)))))) & ((!(((v_princess_1) = ((0+(22)))))) -> ((v_princess_401) = ((0)))))))))) & (((v_princess_2) = (v_princess_403) & (((!(!(((v_princess_1) = ((0+(18))))))) -> ((v_princess_403) = ((143)))) & ((!(((v_princess_1) = ((0+(18)))))) -> ((v_princess_403) = ((0)))))))))))) & (((v_princess_1) = (v_princess_405) & (((!(((i844) = ((0+(1)))))) -> ((v_princess_405) = (v_princess_0))) & ((((i844) = ((0+(1))))) -> ((v_princess_405) = ((18)))))))))) &
\part[right](((v_princess_0) = (v_princess_407) & (((!(((i844) = ((0+(1)))))) -> ((v_princess_407) = ((22)))) & ((((i844) = ((0+(1))))) -> ((v_princess_407) = ((17))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 -> false
}
\functions {
int v_princess_407;
int v_princess_405;
int v_princess_403;
int v_princess_401;
int v_princess_399;
int v_princess_397;
int v_princess_395;
int v_princess_393;
int v_princess_391;
int v_princess_389;
int v_princess_387;
int v_princess_385;
int v_princess_383;
int v_princess_381;
int v_princess_379;
int v_princess_377;
int v_princess_375;
int v_princess_373;
int v_princess_371;
int v_princess_369;
int v_princess_367;
int v_princess_365;
int v_princess_363;
int v_princess_361;
int v_princess_359;
int v_princess_357;
int v_princess_355;
int v_princess_353;
int v_princess_351;
int v_princess_349;
int v_princess_347;
int v_princess_345;
int v_princess_343;
int v_princess_341;
int v_princess_339;
int v_princess_337;
int v_princess_335;
int v_princess_333;
int v_princess_331;
int v_princess_329;
int v_princess_327;
int v_princess_325;
int v_princess_323;
int v_princess_321;
int v_princess_319;
int v_princess_317;
int v_princess_315;
int v_princess_313;
int v_princess_311;
int v_princess_309;
int v_princess_307;
int v_princess_305;
int v_princess_303;
int v_princess_301;
int v_princess_299;
int v_princess_297;
int v_princess_295;
int v_princess_293;
int v_princess_291;
int v_princess_289;
int v_princess_287;
int v_princess_285;
int v_princess_283;
int v_princess_281;
int v_princess_279;
int v_princess_277;
int v_princess_275;
int v_princess_273;
int v_princess_271;
int v_princess_269;
int v_princess_267;
int v_princess_265;
int v_princess_263;
int v_princess_261;
int v_princess_259;
int v_princess_257;
int v_princess_255;
int v_princess_253;
int v_princess_251;
int v_princess_249;
int v_princess_247;
int v_princess_245;
int v_princess_243;
int v_princess_241;
int v_princess_239;
int v_princess_237;
int v_princess_235;
int v_princess_233;
int v_princess_231;
int v_princess_229;
int v_princess_227;
int v_princess_225;
int v_princess_223;
int v_princess_221;
int v_princess_219;
int v_princess_217;
int v_princess_215;
int v_princess_213;
int v_princess_211;
int v_princess_209;
int v_princess_207;
int v_princess_205;
int v_princess_203;
int v_princess_201;
int v_princess_199;
int v_princess_197;
int v_princess_195;
int v_princess_193;
int v_princess_191;
int v_princess_189;
int v_princess_187;
int v_princess_185;
int v_princess_183;
int v_princess_181;
int v_princess_179;
int v_princess_177;
int v_princess_175;
int v_princess_173;
int v_princess_171;
int v_princess_169;
int v_princess_167;
int v_princess_165;
int v_princess_163;
int v_princess_161;
int v_princess_159;
int v_princess_157;
int v_princess_155;
int v_princess_153;
int v_princess_151;
int v_princess_149;
int v_princess_147;
int v_princess_145;
int v_princess_143;
int v_princess_141;
int v_princess_139;
int v_princess_136;
int v_princess_135;
int v_princess_134;
int v_princess_133;
int v_princess_132;
int v_princess_131;
int v_princess_130;
int v_princess_129;
int v_princess_128;
int v_princess_127;
int v_princess_126;
int v_princess_125;
int v_princess_124;
int v_princess_123;
int v_princess_122;
int v_princess_121;
int v_princess_120;
int v_princess_119;
int v_princess_118;
int v_princess_117;
int v_princess_116;
int v_princess_115;
int v_princess_114;
int v_princess_113;
int v_princess_112;
int v_princess_111;
int v_princess_110;
int v_princess_109;
int v_princess_108;
int v_princess_107;
int v_princess_106;
int v_princess_105;
int v_princess_104;
int v_princess_103;
int v_princess_102;
int v_princess_101;
int v_princess_100;
int v_princess_99;
int v_princess_98;
int v_princess_97;
int v_princess_96;
int v_princess_95;
int v_princess_94;
int v_princess_93;
int v_princess_92;
int v_princess_91;
int v_princess_90;
int v_princess_89;
int v_princess_88;
int v_princess_87;
int v_princess_86;
int v_princess_85;
int v_princess_84;
int v_princess_83;
int v_princess_82;
int v_princess_81;
int v_princess_80;
int v_princess_79;
int v_princess_78;
int v_princess_77;
int v_princess_76;
int v_princess_75;
int v_princess_74;
int v_princess_73;
int v_princess_72;
int v_princess_71;
int v_princess_70;
int v_princess_69;
int v_princess_68;
int v_princess_67;
int v_princess_66;
int v_princess_65;
int v_princess_64;
int v_princess_63;
int v_princess_62;
int v_princess_61;
int v_princess_60;
int v_princess_59;
int v_princess_58;
int v_princess_57;
int v_princess_56;
int v_princess_55;
int v_princess_54;
int v_princess_53;
int v_princess_52;
int v_princess_51;
int v_princess_50;
int v_princess_49;
int v_princess_48;
int v_princess_47;
int v_princess_46;
int v_princess_45;
int v_princess_44;
int v_princess_43;
int v_princess_42;
int v_princess_41;
int v_princess_40;
int v_princess_39;
int v_princess_38;
int v_princess_37;
int v_princess_36;
int v_princess_35;
int v_princess_34;
int v_princess_33;
int v_princess_32;
int v_princess_31;
int v_princess_30;
int v_princess_29;
int v_princess_28;
int v_princess_27;
int v_princess_26;
int v_princess_25;
int v_princess_24;
int v_princess_23;
int v_princess_22;
int v_princess_21;
int v_princess_20;
int v_princess_19;
int v_princess_18;
int v_princess_17;
int v_princess_16;
int v_princess_15;
int v_princess_14;
int v_princess_13;
int v_princess_12;
int v_princess_11;
int v_princess_10;
int v_princess_9;
int v_princess_8;
int v_princess_7;
int v_princess_6;
int v_princess_5;
int v_princess_4;
int v_princess_3;
int v_princess_2;
int v_princess_1;
int v_princess_0;
}
\predicates {
v_princess_137;
}
\interpolant{left; right}
